T:Type, x:T, L:T List, P:((||L||+1)).
filter2(P;x.L) = if P(0) x.filter2(i.P(i+1);L) else filter2(i.P(i+1);L) fi  T List 

latex

Definitions	t  T, , x:A. B(x), ||as||, {i..j}, b, A, b, Prop, ij, P  Q, False, AB, P & Q, i  j < k, P  Q, Unit, filter2(P;L), if b t else f fi, , reduce2(f;k;i;as), True, T
Lemmas	squash wf, true wf, reduce2 wf, reduce2 shift, le wf, ifthenelse wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, non neg length, bnot wf, not wf, assert wf, int seg wf, length wf1, bool wf